I suppose &"foo" <|> ... should trigger a token match just as well. Which begs the question of how to handle

syntax discharger := atomic(" (" (&"discharger" <|> &"disch")) " := " tacticSeq ")"

The simplest solution would be to define

syntax dischTk := &"discharger" <|> &"disch"

and then use $_:dischTk. It would basically be the reverse of the previous situation: introduce intermediary syntax when you do not want to match the token.

I think for discharger, we can just remove the disch variant. Generally, adding an extra syntax node sounds good.

I'm still unsure what to do about something like

syntax unifConstraint := term (" =?= " <|> " ≟ ") term

In built-in syntax this would be unicodeSymbol, but we can't make that a parser alias as it takes two strings, not parsers. By the above we could do

syntax unifTk := " =?= " <|> " ≟ "

but then we would have to write $_:unifTk in patterns instead. Do we want to keep the pattern irrelevance in these cases? Then we could also introduce a generic parser combinator, as I think was proposed before, like

syntax unifTk := nomatch (" =?= " <|> " ≟ ")

except maybe with a better name.

The one-size-fits-all solution for when ParserDescr is not expressive enough is to make a parser alias. I think this also depends on (y)our long-term plans: do we want to get rid of ParserDescr or get rid of Parser? As it stands, we're running into ParserDescr limitations left and right (e.g. we can't expose sepByIndent either because it takes a string and a parser, and I'm not even getting into optional arguments).

We've discussed the nomatch before, such a feature would also be great for sepByIndent, etc. Here the nomatch should be outside of the unifTk though, we don't want to check the kind of the unifTk node.

do we want to get rid of ParserDescr

I do!

Here the nomatch should be outside of the unifTk though, we don't want to check the kind of the unifTk node.

Ah, you're right. Unless someone can think of a better name, I'd probably go with that.